//  Copyright 2011 Charlie Garrett
//
//  Licensed under the Apache License, Version 2.0 (the "License");
//  you may not use this file except in compliance with the License.
//  You may obtain a copy of the License at
//
//  http://www.apache.org/licenses/LICENSE-2.0
//
//  Unless required by applicable law or agreed to in writing, software
//  distributed under the License is distributed on an "AS IS" BASIS,
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//  See the License for the specific language governing permissions and
//  limitations under the License.
//
//  Interpreter.cpp
//

#include <stack>
#include <sstream>

#include "Interpreter.h"
#include "Register.h"

namespace logic {    
    using namespace std;
    
    bool Interpreter::Cell::IsRef() const {
        return (type == REF);
    }
    
    bool Interpreter::Cell::IsBoundRef() const {
        if (type == REF) {
            assert(value.cell != NULL);
            return (value.cell != this);
        }
        return false;
    }
    
    bool Interpreter::Cell::IsUnboundRef() const {
        if (type == REF) {
            assert(value.cell != NULL);
            return (value.cell == this);
        }
        return false;
    }
    
    void Interpreter::Cell::UnbindRef() {
        // REF cells may be "bound" by overwriting them with CONSTANTs.
        assert(type == REF || type == CONSTANT);
        type = REF;
        value.cell = this;
    }
    
    bool Interpreter::Cell::Equals(const Interpreter::Cell &other) {
        if (type != other.type) {
            return false;
        }
        switch (type) {
            case REF:
            case STR:
            case LIST:
                return (value.cell == other.value.cell);
            case FUNCTOR:
                return value.functor->Equals(*other.value.functor);
            case CONSTANT: {
                Value result = (*value.constant) == (*other.value.constant);
                return result.data.boolean;
            }
        }
    }
    
    // Dereference addr until it terminates in an unbound REF cell
    // or an STR cell.
    Interpreter::Cell *Interpreter::Cell::deref() const {
        Cell *addr = const_cast<Cell*>(this);
        while (addr->IsBoundRef()) {
            addr = addr->value.cell;
        }
        assert(addr->type != FUNCTOR);
        return addr;
    }
    
    string Interpreter::Cell::ToString() const {
        ostringstream os;
        switch (type) {
            case REF:
                os << "REF 0x" << hex << (unsigned long) value.cell << dec;
                // os << "    " << DebugMessage();
                break;
            case STR:
                os << "STR 0x" << hex << (unsigned long) value.cell << dec;
                // os << "    " << DebugMessage();
                break;
            case FUNCTOR:
                os << value.functor->ToString();
                break;
            case CONSTANT:
                os << value.constant->ToString();
                break;
            case LIST:
                os << "LIST 0x" << hex << (unsigned long) value.cell << dec;
                break;
        }
        return os.str();
    }
    
    string Interpreter::Cell::DebugMessage(const Cell *upper_bound) const {
        switch (type) {
            case REF:
                // TODO: Associate variable names with REF cells.
                if (value.cell == this) {
                    return "<UNBOUND>";
                } else {
                    ostringstream os;
                    os << value.cell->DebugMessage(upper_bound);
                    return os.str();
                }
            case STR: {
                ostringstream os;
                Interpreter::Cell *functor_cell = value.cell;
                assert(functor_cell->type == FUNCTOR);
                const Functor *functor = functor_cell->value.functor;
                unsigned arity = functor->GetArity();
                if (arity == 0) {
                    return functor->GetName();
                } else {
                    os << functor->GetName() + "(";
                    for (int i = 1; i <= arity; i++) {
                        if (functor_cell + i < upper_bound) {
                            os << (functor_cell + i)->DebugMessage(upper_bound);
                        } else {
                            os << "<oob>";
                        }
                        if (i < arity) {
                            os << ", ";
                        }
                    }
                    os << ")";
                    return os.str();
                }
            }
            case FUNCTOR:
                return value.functor->ToString();
            case CONSTANT:
                return value.constant->ToString();
            case LIST:
                return "[|]";
        }
    }
    
    Interpreter::Cell *Interpreter::State::CopyCell(const Cell &cell) {
        if (H < MAX_HEAP_SIZE) {
            Cell *new_cell = &HEAP[H++];
            (*new_cell) = cell;
            return new_cell;
        } else {
            return NULL;
        }
    }
    
    Interpreter::Environment::Environment(size_t CE_, vector<Instruction*>::iterator CP_, size_t num_vars) :
        CE(CE_), CP(CP_) {
        num_permanent_vars = num_vars;
        Y.resize(num_permanent_vars);
    }
    
    string Interpreter::Environment::ToString() {
        ostringstream os;
        os << "Environment Frame" << endl;
        os << "CE = " << CE << endl;
        // os << "CP = " << (*CP)->ToString() << endl;
        os << num_permanent_vars << " permanent variables" << endl;
        for (vector<Cell>::iterator it = Y.begin(); it != Y.end(); ++it) {
            os << it->ToString() << endl;
        }
        return os.str();
    }
    
    Interpreter::ChoicePoint::ChoicePoint(size_t E_, size_t B_, size_t TR_, size_t H_,
                                          vector<Instruction*>::iterator BP_,
                                          vector<Instruction*>::iterator CP_) :
        E(E_), B(B_), TR(TR_), H(H_), BP(BP_), CP(CP_) {
    }
    
    string Interpreter::ChoicePoint::ToString() {
        ostringstream os;
        os << "Choice Point Frame" << endl;
        os << "E = " << E << endl;
        os << "B = " << B << endl;
        os << "TR = " << TR << endl;
        os << "H = " << H << endl;
        os << A.size() << " arguments" << endl;
        for (vector<Cell>::iterator it = A.begin(); it != A.end(); ++it) {
            os << it->ToString() << endl;
        }
        return os.str();
    }
    
    Interpreter::Environment *Interpreter::CreateEnvironment(size_t num_vars) {
        return new Interpreter::Environment(state.E, state.CP, num_vars);
    }
    
    Interpreter::ChoicePoint *Interpreter::CreateChoicePoint(size_t next_clause_offset) {
        vector<Instruction*>::iterator BP = state.code.begin() + next_clause_offset;
        ChoicePoint *choice_point =
            new Interpreter::ChoicePoint(state.E, state.B, state.TR, state.H, BP, state.CP);
        assert(state.num_args <= state.A.size());
        for (int n = 0; n < state.num_args; n++) {
            choice_point->A.push_back(state.A.at(n));
        }
        return choice_point;
    }
    
    void Interpreter::RetryFromChoicePoint(ChoicePoint *choice_point, size_t next_clause_offset) {
        // Restore argument registers.
        for (int n = 0; n < choice_point->A.size(); n++) {
            state.A[n] = choice_point->A.at(n);
        }
        // Restore machine control registers.
        state.E = choice_point->E;
        state.CP = choice_point->CP;
        choice_point->BP = state.code.begin() + next_clause_offset;
        unwind_trail(choice_point->TR, state.TR);
        state.TR = choice_point->TR;
        state.H = choice_point->H;
    }

    void Interpreter::State::Print() const {
        cout << "Heap with " << H << " cells." << endl;
        for (unsigned i = 0; i < H; i++) {
            cout << "  [0x" << hex << (unsigned long) &HEAP[i] <<
            "]  " << i << ": " << dec << HEAP[i].ToString() << endl;
        }
        
        cout << endl;
        cout << "Stack with " << STACK.size() << " frames." << endl;
        if (!STACK.empty()) {
            cout << STACK.back()->ToString() << endl;
        }
        
        cout << endl;
        cout << X.size() << " X registers." << endl;
        for (unsigned reg = 0; reg < X.size(); ++reg) {
            cout << "  X" << reg << " = ";
            cout << X.at(reg).ToString() << endl;
        }
        cout << endl;

        cout << A.size() << " A registers." << endl;
        for (unsigned reg = 0; reg < A.size(); ++reg) {
            cout << "  A" << reg << " = ";
            cout << A.at(reg).ToString() << endl;
        }
        cout << endl;
        
        cout << "Machine registers" << endl;
        cout << "H = " << H << endl;
        cout << "E = " << E << endl;
        cout << "B = " << B << endl;
        cout << "TR = " << TR << endl;
        cout << "HB = " << HB << endl;
        cout << "S = 0x" << hex << (unsigned long) S << dec << endl;
        cout << "fail = " << fail << endl;
        cout << endl;
        
        cout << "Answer substitution:" << endl;
        for (map<Variable*, Cell>::const_iterator ans = answer_substitution.begin();
             ans != answer_substitution.end(); ++ans) {
            cout << ans->first->ToString()
                 << " = " << ans->second.ToString()
                 << " " << ans->second.deref()->ToString()
                 << " " << ans->second.DebugMessage(&HEAP[H]) << endl;
        }
        cout << endl;
    }

    void Interpreter::State::PrintAnswer() const {
        if (fail) {
            cout << "false";
        } else {
            if (answer_substitution.empty()) {
                cout << "true";
            } else {
                for (map<Variable*, Cell>::const_iterator ans = answer_substitution.begin();
                     ans != answer_substitution.end(); ++ans) {
                    cout << ans->first->ToString()
                         << " = " << ans->second.ToString()
                         << " " << ans->second.deref()->ToString()
                         << " " << ans->second.DebugMessage(&HEAP[H]) << endl;
                }
            }
        }
    }
    
    // Register accessors.
    Interpreter::Cell &Interpreter::GetReg(Register reg) {
        switch (reg.kind) {
            case Register::UNALLOCATED:
                assert(false);
            case Register::TEMPORARY:
                return state.X.at(reg.number);
            case Register::PERMANENT:
                return state.TopEnvironmentFrame()->Y.at(reg.number);
            case Register::ARGUMENT:
                return state.A.at(reg.number);
        }
    }
    
    void Interpreter::SetReg(Register reg, const Cell &cell) {
        switch (reg.kind) {
            case Register::UNALLOCATED:
                assert(false);
                break;
            case Register::TEMPORARY:
                if (reg.number >= state.X.size()) {
                    state.X.resize(reg.number + 1);
                }
                state.X.at(reg.number) = cell;
                break;
            case Register::PERMANENT:
                assert(reg.number < state.TopEnvironmentFrame()->Y.size());
                state.TopEnvironmentFrame()->Y.at(reg.number) = cell;
                break;
            case Register::ARGUMENT:
                if (reg.number >= state.A.size()) {
                    state.A.resize(reg.number + 1);
                }
                state.A.at(reg.number) = cell;
                break;
        }
    }
    
    void Interpreter::CopyReg(Register from, Register to) {
        SetReg(to, GetReg(from));
    }
    
    // Return an unbound variable REF cell.
    Interpreter::Cell *Interpreter::CreateRefCell() {
        Cell *result = state.GetNextCell();
        if (result != NULL) {
            result->type = Cell::REF;
            result->value.cell = result;
        }
        return result;
    }
    
    // Return a variable REF cell bound to the argument Cell.
    Interpreter::Cell *Interpreter::CreateRefCell(Cell *cell) {
        Cell *result = state.GetNextCell();
        if (result != NULL) {
            result->type = Cell::REF;
            result->value.cell = cell;
        }
        return result;
    }
    
    // Return an uninitialized STR cell.
    Interpreter::Cell *Interpreter::CreateStrCell() {
        Cell *result = state.GetNextCell();
        if (result != NULL) {
            result->type = Cell::STR;
            result->value.cell = NULL;
        }
        return result;
    }
    
    // Return a FUNCTOR cell initialized to the argument functor.
    Interpreter::Cell *Interpreter::CreateFunctorCell(const Functor *functor) {
        Cell *result = state.GetNextCell();
        if (result != NULL) {
            result->type = Cell::FUNCTOR;
            result->value.functor = functor;
        }
        return result;
    }
    
    // Return a LIST cell pointing to the argument cell.
    Interpreter::Cell *Interpreter::CreateListCell(Cell *element) {
        Cell *result = state.GetNextCell();
        if (result != NULL) {
            result->type = Cell::LIST;
            result->value.cell = element;
        }
        return result;
    }
    
    // Copy Cell value onto the heap.
    Interpreter::Cell *Interpreter::CopyCell(const Cell &cell) {
        return state.CopyCell(cell);
    }
    
    void Interpreter::InitState(bool clear_code) {
        // Create a initialized interpreter state
        state.H = 0;
        state.X.clear();
        state.A.clear();
        
        // Clear both environment and choice point frames.
        while (!state.STACK.empty()) {
            Frame *frame = state.STACK.back();
            state.STACK.pop_back();
            delete frame;
        }
        state.STACK.clear();
        state.E = -1;
        state.B = -1;
        
        state.TRAIL.clear();
        state.TR = 0;
        
        state.HB = 0;
        
        // Initialize structure matching.
        state.mode = State::UNIFY_READ;
        state.S = 0;
        
        state.fail = false;
        
        state.num_args = 0;
        
        if (clear_code) {
            state.code.clear();
        }
        
        state.answer_substitution.clear();
        
        // Place a bottommost choice point on the stack.
        state.STACK.push_back(CreateChoicePoint(0));
        state.B = State::BOTTOM_OF_STACK;
    }

    void Interpreter::PrintCode() {
        cout << endl << "Interpreter code" << endl;
        for (vector<Instruction*>::iterator inst = state.code.begin(); inst != state.code.end(); ++inst) {
            cout << (*inst)->ToString() << endl;
        }
    }
    
    void Interpreter::PrintState() {
        state.Print();
    }
    
    void Interpreter::PrintAnswer() {
        state.PrintAnswer();
    }
    
    // Run the program in the Code section of the interpreter.
    bool Interpreter::Run() {
        return RunFrom(0);
    }
    
    // Run the program from a specific code offset.
    bool Interpreter::RunFrom(size_t code_offset) {
        state.P = state.code.begin() + code_offset;
        return Continue();
    }
    
    // Continue execution from the current program counter, state.P, until
    // a goal succeeds or fails.
    // Returns true if the interpreter runs to completion, regardless of whether
    // the goal succeeds, and false if the interpreter gets stuck.
    bool Interpreter::Continue() {
        // Instructions update state.P to point to their successor.
        for (; state.P != state.code.end(); ) {
            if (trace) {
                cout << "Executing: " << (*state.P)->ToString() << endl;
            }
            if (!(*state.P)->Execute(this)) {
                cout << "Error executing instruction!" << endl;
                return false;
            }
            if (state.fail) {
                if (trace) {
                    cout << "GOAL FAILED!" << endl;
                }
                break;
            }
            if (trace) {
                PrintState();
            }
        }
        if (!state.fail && trace) {
            cout << "GOAL SUCCEEDED!" << endl;
        }
        return true;
    }
    
    // Return true if the interpreter has executed a query and may possibly have
    // another answer through backtracking and false otherwise.
    bool Interpreter::MoreAnswers() {
        if (state.fail) {
            return false;
        }
        if (state.code.empty()) {
            return false;
        }
        if (state.B == -1 || state.B == State::BOTTOM_OF_STACK) {
            return false;
        }
        return true;
    }

    // Backtrack and try to find more solutions to a query.
    bool Interpreter::FailAndContinue() {
        assert(MoreAnswers());
        backtrack();
        return Continue();
    }
    
    // WAM utility routines
    
    // If there is a choice point on the stack, backtrack to it by setting the program
    // pointer and clearing the fail flag.  If there is no valid choice point, then
    // prepare to exit the program with failure.
    void Interpreter::backtrack() {
        if (state.B != State::BOTTOM_OF_STACK) {
            ChoicePoint *choice_point = state.TopChoicePoint();
            // state.B0 = choice_point->B0;
            state.P = choice_point->BP;
            state.fail = false;
        }
    }
    
    // Take two heap cells, at least one of which must be an unbound REF.
    // Bind the unbound REF to the other cell.  Break ties in favor of
    // the cell with the lower address.
    void Interpreter::bind(Interpreter::Cell *addr, Interpreter::Cell *ref) {
        assert(addr->IsUnboundRef() || ref->IsUnboundRef());
        if (addr->IsUnboundRef() && (!ref->IsRef() || addr->value.cell < ref->value.cell)) {
            addr->value.cell = ref;
            trail(addr);
        } else if (ref->IsUnboundRef()) {
            ref->value.cell = addr;
            trail(ref);
        } else {
            assert(false);
        }
    }
    
    // Trail, or remember the binding of, a REF cell.  This permits undoing the binding
    // later in unwind_trail.
    void Interpreter::trail(Interpreter::Cell *cell) {
        // We must trail every binding that was on the heap before the most recent
        // choice point was created (i.e. less than HB) or that was on the stack
        // before the most recent choice point was created (i.e. in a frame lower
        // than B).  We can conservatively trail all bindings for now.
        // TODO: Only trail the required cells.
        state.TRAIL.push_back(cell);
        state.TR++;
    }
    
    // Clear the bindings of all cells in TRAIL in the range [low, high).
    void Interpreter::unwind_trail(size_t low, size_t high) {
        assert(low <= high);
        for (size_t i = low; i < high; i++) {
            state.TRAIL[i]->UnbindRef();
        }
        state.TRAIL.resize(low);
    }
    
    // Unify two heap cells.
    // TODO: All values to be unified come in pairs here.  Should we make a stack of pairs?
    void Interpreter::unify(Interpreter::Cell *addr1, Interpreter::Cell *addr2) {
        stack<Interpreter::Cell*> pdl;
        pdl.push(addr1);
        pdl.push(addr2);
        state.fail = false;
        while (!(pdl.empty() || state.fail)) {
            Interpreter::Cell *deref2 = pdl.top()->deref();
            pdl.pop();
            Interpreter::Cell *deref1 = pdl.top()->deref();
            pdl.pop();
            if (!deref1->Equals(*deref2)) {
                switch (deref1->type) {
                    case Cell::REF:
                        bind(deref1, deref2);
                        break;
                    case Cell::STR:
                        if (deref2->type == Cell::REF) {
                            bind(deref1, deref2);
                        } else if (deref2->type == Cell::STR) {
                            Cell *functor1 = deref1->value.cell;
                            Cell *functor2 = deref2->value.cell;
                            assert(functor1->type == Cell::FUNCTOR);
                            assert(functor2->type == Cell::FUNCTOR);
                            if (functor1->value.functor->Equals(*functor2->value.functor)) {
                                for (int i = 1; i <= functor1->value.functor->arity; i++) {
                                    pdl.push(functor1 + i);
                                    pdl.push(functor2 + i);
                                }
                            } else {
                                state.fail = true;
                            }
                        } else {
                            state.fail = true;
                        }
                        break;
                    case Cell::CONSTANT:
                        if (deref2->type == Cell::REF) {
                            bind(deref1, deref2);
                        } else {
                            // Only identical constants unify and the equality
                            // test above failed.
                            state.fail = true;
                        }
                        break;
                    case Cell::LIST:
                        if (deref2->type == Cell::REF) {
                            bind(deref1, deref2);
                        } else if (deref2->type == Cell::LIST) {
                            // Lists are functors with two arguments.
                            pdl.push(deref1->value.cell);
                            pdl.push(deref2->value.cell);
                            pdl.push(deref1->value.cell + 1);
                            pdl.push(deref2->value.cell + 1);
                        } else {
                            state.fail = true;
                        }
                        break;
                    case Cell::FUNCTOR:
                        assert(false);
                        break;
                }
            }
        }
    }
        
    // Build the representation of an unbound variable on the heap and copy
    // its Cell into a normal register and an argument register.  Return true
    // if we succeed and false if we fail.
    // In pseudocode:
    //    put_variable Xn, Ai = HEAP[H] <- <REF, H>;
    //                          Xn <- HEAP[H];
    //                          Ai <- HEAP[H];
    //                          H <- H + 1;
    bool Interpreter::put_variable(Register reg, Register arg_reg) {
        Cell *cell = CreateRefCell();
        if (cell != NULL) {
            SetReg(reg, *cell);
            SetReg(arg_reg, *cell);
            state.P++;
            return true;
        } else {
            return false;
        }
    }
    
    // Copy the value from a normal register to an argument register.
    // In pseudocode:
    //    put_value Xn, Ai = Ai <- Xn
    bool Interpreter::put_value(Register reg, Register arg_reg) {
        CopyReg(reg, arg_reg);
        state.P++;
        return true;
    }
    
    // Build the representation of a structure on the heap and copy its Cell
    // into the argument register.  Return true if we succeed and false if we fail.
    // We omit the extraneous <STR, N> cell before each functor.
    // In pseudocode:
    //    put_structure f/n, Ai = HEAP[H] <- f/n;
    //                            Ai <- HEAP[H];
    //                            H <- H + 1;
    bool Interpreter::put_structure(const Functor *functor, Register arg_reg) {
        Cell *functor_cell = CreateFunctorCell(functor);
        if (functor_cell != NULL) {
            Cell str_cell(Cell::STR, functor_cell);
            SetReg(arg_reg, str_cell);
            state.P++;
            return true;
        } else {
            return false;
        }
    }
    
    // Place a list Cell into the argument register, with the list's first element
    // pointing to the top of the heap.
    // In pseudocode:
    //    put_list Ai = Ai <- <LIS, H>;
    bool Interpreter::put_list(Register arg_reg) {
        Cell list_cell(Cell::LIST, &state.HEAP[state.H]);
        SetReg(arg_reg, list_cell);
        state.P++;
        return true;
    }
    
    // Place a constant Cell directly into an argument register, bypassing
    // the heap entirely.
    // In pseudocode:
    //    put_constant c, Ai = Ai <- <CON, c>;
    bool Interpreter::put_constant(const Value *constant, Register arg_reg) {
        Cell const_cell(constant);
        SetReg(arg_reg, const_cell);
        state.P++;
        return true;
    }
    
    // Copy the value from an argument register to a normal register.
    // In pseudocode:
    //    get_variable Ai, Xn = Xn <- Ai
    bool Interpreter::get_variable(Register reg, Register arg_reg) {
        CopyReg(arg_reg, reg);
        state.P++;
        return true;        
    }
    
    // Unify the contents of a normal register and an argument register.
    // In pseudocode:
    //    get_value Xn, Ai = unify(Xn, Ai);
    //                       if fail
    //                          then backtrack
    //                          else P <- P + instruction_size(P)
    bool Interpreter::get_value(Register reg, Register arg_reg) {
        unify(&GetReg(reg), &GetReg(arg_reg));
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;
    }
    
    // Unify a structure on the heap with a query already on the heap and
    // stored in X0.  Set the interpreter's fail flag if unification fails.
    // In pseudocode:
    //    get_structure f/n, Xi = addr <- deref(Xi);
    //                            case STORE[addr] of
    //                               <REF, _> : HEAP[H] <- <STR, H + 1>;
    //                                          HEAP[H + 1] <- f/n;
    //                                          bind(addr, H);
    //                                          H = H + 2;
    //                                          mode <- write;
    //                               <STR, a> : if HEAP[a] = f/n
    //                                             then
    //                                               begin
    //                                                 S <- a + 1;
    //                                                 mode <- read;
    //                                               end
    //                                             else fail <- true;
    //                               other    : fail <- true;
    //                            endcase
    //                            if fail
    //                               then backtrack
    //                               else P <- P + instruction_size(P);
    bool Interpreter::get_structure(const Functor *functor, Register reg) {
        Cell *addr = GetReg(reg).deref();
        switch (addr->type) {
            case Cell::REF: {
                // An unbound reference, so we will write on the heap.
                Cell *str_cell = CreateStrCell();
                Cell *functor_cell = CreateFunctorCell(functor);
                if (str_cell == NULL || functor_cell == NULL) {
                    return false;
                }
                str_cell->value.cell = functor_cell;
                bind(addr, str_cell);
                state.mode = State::UNIFY_WRITE;
                break;
            }
            case Cell::STR: {
                Cell *functor_cell = addr->value.cell;
                assert(functor_cell->type == Cell::FUNCTOR);
                if (functor->Equals(*functor_cell->value.functor)) {
                    state.S = functor_cell + 1;
                    state.mode = State::UNIFY_READ;
                } else {
                    state.fail = true;
                }
                break;
            }
            case Cell::FUNCTOR:
            case Cell::CONSTANT:
            case Cell::LIST:
                state.fail = true;
                break;
        }
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;
    }
    
    // Unify the argument register with a list, either placing a list
    // cell on the heap or matching against it.
    // In pseudocode:
    //    get_list Ai = addr <- deref(Ai);
    //                  case STORE[addr] of
    //                     <REF, _>  : STORE[addr] <- <LIS, H + 1>;
    //                                 bind(addr, H);
    //                                 H <- H + 1;
    //                                 mode <- write;
    //                     <LIS, a>  : S <- a;
    //                                 mode <- read;
    //                     other     : fail <- true;
    //                  endcase;
    //                  if fail
    //                     then backtrack
    //                     else P <- P + instruction_size(P);
    bool Interpreter::get_list(Register arg_reg) {
        Cell *addr = GetReg(arg_reg).deref();
        switch (addr->type) {
            case Cell::REF: {
                // An unbound reference, so we will write on the heap.
                Cell *list_cell = CreateListCell(&state.HEAP[state.H + 1]);
                if (list_cell == NULL) {
                    return false;
                }
                bind(addr, list_cell);
                state.mode = State::UNIFY_WRITE;
                break;
            }
            case Cell::LIST:
                state.S = addr->value.cell;
                state.mode = State::UNIFY_READ;
                break;
            case Cell::STR:
            case Cell::FUNCTOR:
            case Cell::CONSTANT:
                state.fail = true;
                break;
        }
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;        
    }
    
    // Unify the argument register with the constant value, either placing
    // the constant on the heap or matching against it.
    // In pseudocode:
    //    get_constant c, Ai = addr <- deref(Ai);
    //                         case STORE[addr] of
    //                            <REF, _>  : STORE[addr] <- <CON, c>;
    //                                        trail(addr);
    //                            <CON, c'> : fail <- (c != c');
    //                            other     : fail <- true;
    //                         endcase;
    //                         if fail
    //                            then backtrack
    //                            else P <- P + instruction_size(P);
    bool Interpreter::get_constant(const Value *constant, Register arg_reg) {
        Cell const_cell(constant);
        Cell *addr = GetReg(arg_reg).deref();
        switch (addr->type) {
            case Cell::REF:
                // Instead of binding the reference cell, we simply overwrite
                // it with a constant!
                (*addr) = constant;
                trail(addr);
                break;
            case Cell::CONSTANT:
                if (!const_cell.Equals(*addr)) {
                    state.fail = true;
                }
                break;
            case Cell::STR:
            case Cell::FUNCTOR:
            case Cell::LIST:
                state.fail = true;
                break;
        }
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;
    }
        
    // Build the representation of a unbound variable on the heap and copy
    // its Cell into the register.  Return true if we succeed and false if
    // we fail.
    // In pseudocode:
    //    set_variable Xi = HEAP[H] <- <REF, H>;
    //                      Xi <- HEAP[H];
    //                      H <- H + 1;
    bool Interpreter::set_variable(Register reg) {
        Cell *cell = CreateRefCell();
        if (cell != NULL) {
            SetReg(reg, *cell);
            state.P++;
            return true;
        } else {
            return false;
        }
    }
    
    // Build the representation of a bound variable on the heap and copy
    // its Cell into the register.
    // In pseudocode:
    //    set_value Xi = HEAP[H] <- Xi;
    //                   H <- H + 1;
    bool Interpreter::set_value(Register reg) {
        if (CopyCell(GetReg(reg)) != NULL) {
            state.P++;
            return true;
        } else {
            return false;
        }
    }
    
    // Place the constant value on top of the heap.
    // In pseudocode:
    //    set_constant c = HEAP[H] <- <CON, c>;
    //                     H <- H + 1;
    bool Interpreter::set_constant(const Value *constant) {
        Cell const_cell(constant);
        if (CopyCell(const_cell) != NULL) {
            state.P++;
            return true;
        } else {
            return false;
        }
    }
    
    // Push N unbound REF cells onto the heap.
    // In pseudocode:
    //    for i <- H to H + n - 1 do
    //      HEAP[i] <- <REF, i>;
    //    H <- H + n;
    bool Interpreter::set_void(size_t N) {
        for (int i = 0; i < N; i++) {
            if (CreateRefCell() == NULL) {
                return false;
            }
        }
        state.P++;
        return true;
    }

    // Unify the current structure in read mode or unify a new variable
    // in write mode.  Return true if we succeed and false if we fail.
    // In pseudocode:
    //    unify_variable Xi = case mode of
    //                           read : Xi <- HEAP[S];
    //                           write: HEAP[H] <- <REF, H>;
    //                                  Xi <- HEAP[H];
    //                                  H <- H + 1;
    //                        endcase;
    //                        S <- S + 1;
    bool Interpreter::unify_variable(Register reg) {
        switch (state.mode) {
            case State::UNIFY_READ:
                SetReg(reg, *state.S++);
                state.P++;
                return true;
            case State::UNIFY_WRITE:
                Cell *cell = CreateRefCell();
                if (cell != NULL) {
                    SetReg(reg, *cell);
                    state.S++;
                    state.P++;
                    return true;
                } else {
                    return false;
                }
        }
    }
    
    // Unify register Xi with the current structure in read mode or 
    // put the register value on the heap in write mode.  Set the
    // interpreter's fail flag if we fail.
    // In pseudocode:
    //    unify_value Xi = case mode of
    //                        read : unify(Xi, S);
    //                        write: HEAP[H] <- Xi;
    //                               H <- H + 1;
    //                     endcase;
    //                     S <- S + 1;
    //                     if fail
    //                        then backtrack
    //                        else P <- P + instruction_size(P)
    bool Interpreter::unify_value(Register reg) {
        switch (state.mode) {
            case State::UNIFY_READ:
                unify(&GetReg(reg), state.S);
                break;
            case State::UNIFY_WRITE: {
                if (CopyCell(GetReg(reg)) == NULL) {
                    return false;
                }
            }
        }
        state.S++;
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;
    }
    
    // Unify the constant with the current structure in read mode or put
    // the constant value on the heap in write mode.
    // In pseudocode:
    //    unify_constant c, Ai = case mode of
    //                              read: addr <- deref(S);
    //                                    case STORE[addr] of
    //                                       <REF, _>  : STORE[addr] <- <CON, c>;
    //                                                   trail(addr);
    //                                       <CON, c'> : fail <- (c != c');
    //                                       other     : fail <- true;
    //                                    endcase;
    //                              write : HEAP[H] <- <CON, c>;
    //                                      H <- H + 1;
    //                           endcase;
    //                           S <- S + 1;
    //                           if fail
    //                              then backtrack
    //                              else P <- P + instruction_size(P);
    // 
    bool Interpreter::unify_constant(const Value *constant) {
        Cell const_cell(constant);
        switch (state.mode) {
            case State::UNIFY_READ: {
                Cell *addr = state.S->deref();
                switch (addr->type) {
                    case Cell::REF:
                        // Instead of binding the reference cell, we simply overwrite
                        // it with a constant!
                        (*addr) = constant;
                        trail(addr);
                        break;
                    case Cell::CONSTANT:
                        if (!const_cell.Equals(*addr)) {
                            state.fail = true;
                        }
                        break;
                    case Cell::STR:
                    case Cell::FUNCTOR:
                    case Cell::LIST:
                        state.fail = true;
                        break;
                }
                break;
            }
            case State::UNIFY_WRITE:
                if (CopyCell(constant) == NULL) {
                    return false;
                }
                break;
        }
        state.S++;
        if (state.fail) {
            backtrack();
        } else {
            state.P++;
        }
        return true;
    }
    
    // In write mode, push N new unbound REF cells onto the heap.  In
    // read mode, skip the next N heap cells starting from location S.
    // In pseudocode:
    //    unify_void n = case mode of
    //                      read  : S <- S + n;
    //                      write : for i <- H to H + n - 1 do
    //                                HEAP[i] <- <REF, i>;
    //                              H <- H + n;
    //                   endcase;
    bool Interpreter::unify_void(size_t N) {
        switch (state.mode) {
            case State::UNIFY_READ:
                state.S += N;
                break;
            case State::UNIFY_WRITE:
                for (int i = 0; i < N; i++) {
                    if (CreateRefCell() == NULL) {
                        return false;
                    }
                }
                break;
        }
        state.P++;
        return true;
    }
    
    // Set the program counter to the CODE address for the functor.
    // In pseudocode:
    //    call p/n = if defined(P)
    //                  then
    //                    begin
    //                      CP <- P + instruction_size(P);
    //                      num_args <- n;
    //                      B0 <- B;
    //                      P <- @(p/n);
    //                    end
    //                  else backtrack;
    bool Interpreter::call(size_t code_offset, size_t nargs) {
        // TODO: Check whether the predicate is defined.
        if (code_offset < state.code.size()) {
            state.CP = state.P + 1;
            state.num_args = nargs;
            state.P = state.code.begin() + code_offset;
            return true;
        } else {
            backtrack();
            return true;
        }
    }
    
    // Proceed is a no-op for the L1 interpreter.
    // In pseudocode:
    //    proceed = P <- CP
    bool Interpreter::proceed() {
        state.P = state.CP;
        return true;
    }
    
    // Halt stops the interpreter from executing.
    bool Interpreter::halt() {
        state.P = state.code.end();
        return true;
    }
    
    // Allocate a stack frame for N permanent variables.
    // In pseudocode:
    //    allocate N = if E > B
    //                   then newE <- E + STACK[E + 2] + 3;
    //                   else newE <- B + STACK[B] + 7;
    //                 STACK[newE] <- E;
    //                 STACK[newE + 1] <- CP;
    //                 STACK[newE + 2] <- N;
    //                 E <- newE;
    bool Interpreter::allocate(size_t N) {
        // Since we're using an abstract stack of Frame pointers, there is no
        // need to test whether an environment frame or a choice point frame
        // is on top.
        size_t newE = state.STACK.size();
        state.STACK.push_back(CreateEnvironment(N));
        state.E = newE;
        state.P++;
        return true;
    }
    
    // Pop a frame off of the stack and return to that frame's caller.
    // In pseudocode:
    //    deallocate N = P <- STACK[E + 1];
    //                   E <- STACK[E];
    bool Interpreter::deallocate() {
        Environment *environment = state.TopEnvironmentFrame();
        state.P = environment->CP;
        state.E = environment->CE;
        return true;
    }
    
    // Allocate a new choice point on the stack and set its contents.
    // In pseudocode:
    //    if E > B
    //       then newB <- E + STACK[E + 2] + 3;
    //       else newB <- B + STACK[B] + 7;
    //    STACK[newB] <- num_args;
    //    n <- STACK[newB];
    //    for i <- 1 to n do STACK[newB + i] <- Ai;
    //    STACK[newB + n + 1] <- E;
    //    STACK[newB + n + 2] <- CP;
    //    STACK[newB + n + 3] <- B;
    //    STACK[newB + n + 4] <- L;
    //    STACK[newB + n + 5] <- TR;
    //    STACK[newB + n + 6] <- H;
    //    B <- newB;
    //    HB <- H;
    bool Interpreter::try_me_else(size_t next_clause_offset) {
        // Since we're using an abstract stack of Frame pointers, there is no
        // need to test whether an environment frame or a choice point frame
        // is on top.
        size_t newB = state.STACK.size();
        state.STACK.push_back(CreateChoicePoint(next_clause_offset));
        state.B = newB;
        state.HB = state.H;
        state.P++;
        return true;
    }
    
    // Reset state after a failed clause and prepare to execute the next clause.
    // In pseudocode:
    //    n <- STACK[B];
    //    for i <- 1 to n do Ai <- STACK[B + i];
    //    E <- STACK[B + n + 1];
    //    CP <- STACK[B + n + 2];
    //    STACK[B + n + 4] <- L;
    //    unwind_trail(STACK[B + n + 5], TR);
    //    TR <- STACK[B + n + 5];
    //    H <- STACK[B + n + 6];
    //    HB <- H;
    bool Interpreter::retry_me_else(size_t next_clause_offset) {
        RetryFromChoicePoint(state.TopChoicePoint(), next_clause_offset);
        state.HB = state.H;
        state.P++;
        return true;
    }

    // Reset state after a failed clause and prepare to execute the final clause.
    // In pseudocode:
    //    n <- STACK[B];
    //    for i <- 1 to n do Ai <- STACK[B + i];
    //    E <- STACK[B + n + 1];
    //    CP <- STACK[B + n + 2];
    //    unwind_trail(STACK[B + n + 5], TR);
    //    TR <- STACK[B + n + 5];
    //    H <- STACK[B + n + 6];
    //    B <- STACK[B + n + 3];
    //    HB <- STACK[B + n + 6];   // Not the same as H above because B changed!
    bool Interpreter::trust_me() {
        ChoicePoint *choice_point = state.TopChoicePoint();
        // 0 is just a dummy offset that will be ignored as this choice point is finished.
        RetryFromChoicePoint(state.TopChoicePoint(), 0);
        // Resetting B here changes the top choice point.
        state.B = choice_point->B;
        // This instruction requires a choice point on all stacks, even before
        // a backtracking predicate is called.
        state.HB = state.TopChoicePoint()->H;
        state.P++;
        return true;
    }
    
    // Associate a source level variable with a heap cell
    // in order to retrieve the results of a computation.
    bool Interpreter::link_source_variable(Variable *var, Register reg) {
        state.answer_substitution[var] = GetReg(reg);
        state.P++;
        return true;
    }

}  // namespace logic
